\documentclass[11pt]{report}

%IMPORTANTE comando \hyphenation{ma-cro-istru-zio-ne nitro-idrossil-amminico} definisce all'algoritmo di latex come spezzare una parola non presente nel suo vocabolario!!

%INCLUSIONE DI PACCHETTI
\usepackage{graphicx}
\usepackage{rotating}
\usepackage{array}
\usepackage{longtable}
\usepackage{multirow}
\usepackage{wrapfig} 
\usepackage{lastpage}
\usepackage{fancyhdr}
\usepackage[english]{babel}
\usepackage{amssymb}
%\usepackage[T1]{fontenc}
%\usepackage[latin9]{inputenc}
\usepackage[colorlinks=true]{hyperref} %per indice con link alle pagine
\usepackage[a4paper,portrait,left=2.5cm,right=2.5cm,bindingoffset=5mm]{geometry}
\usepackage[utf8]{inputenc}
\usepackage{color}
%\usepackage{xstring}
\hypersetup{colorlinks,citecolor=black,filecolor=black,linkcolor=red,urlcolor=blue}
\setcounter{secnumdepth}{2} % per numerare anche \subsubsection
\setcounter{tocdepth}{2}% per farlo apparire nell'indice
\frenchspacing
\definecolor{LightMagenta}{cmyk}{0.1,0.8,0,0.1}


%HEADER e FOOTER di tutte le pagine tranne quella in cui compare il titolo del capitolo
\pagestyle{fancy}
\fancyhead{}
\headheight = 54pt
\lhead{Computer Science Theory II}
\lfoot{}
\cfoot{}
\rfoot{Page \thepage{ of} \pageref{LastPage}}
\renewcommand{\headrulewidth}{1pt}
\renewcommand{\footrulewidth}{1pt}
\rhead{\nouppercase{\leftmark}}
\renewcommand{\chaptermark}[1]{\markboth{\thechapter.\ #1}{}}

%HEADER e FOOTER della pagina dove compare il titolo del capitolo
\fancypagestyle{plain}{
%\lhead{\includegraphics[height=50pt]{images/logoUniPd.png}} %IN ALTO A SINISTRA (POTREBBE ANDARE BENE IL LOGO)
\chead{}
\rhead{\bfseries WS2011/12}%\manualeUtenteVer} %IN ALTO A DESTRA
\lfoot{
\begin{tabular}{lc}
Victor A. Arrascue Ayala & Mtr. 3209050\\
Tobias Domhan  & Mtr.  3202957 \\
\end{tabular}
}
\cfoot{}
\rfoot{Page \thepage{ of} \pageref{LastPage}}
\renewcommand{\headrulewidth}{1pt}
\renewcommand{\footrulewidth}{1pt}
}

\fancypagestyle{romano}{
\lhead{}
\chead{}
\rhead{}
\lfoot{}
\cfoot{\thepage}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
}

\fancypagestyle{empty}{
\lhead{}
\chead{}
\rhead{}
\lfoot{}
\cfoot{}
\rfoot{}
\renewcommand{\headrulewidth}{0pt}
\renewcommand{\footrulewidth}{0pt}
}

%PAGINA DI PRESETAZIONE DEL DOCUMENTO
\hyphenation{}
\begin{document}


%\begin{center}
%\thispagestyle{empty}
%\huge\textbf{UNIVERSIT\`A degli Studi di PADOVA}\\[2 cm] %GRUPPO DI APPARTENENZA
%\vspace*{0.5in}
%\LARGE\textbf{Titolo del documento}\\[1.0 cm] %TITOLO DEL DOCUMENTO
%\par\rule{10cm}{.5pt} \par
%{\large 12 Ottobre 2009}   %DATA DI CREAZIONE
%\par\rule{10cm}{.10pt} \par
%\vspace*{1.0in}
%\includegraphics[scale=0.30]{images/logoUniPd.png} \\[2cm] %LOGO GRUPPO
%\Large\textbf{Michele Tonon} %AUTORE
%\par\rule{6cm}{.5pt} \par
%\end{center}



% INDEX
%\newpage
%\thispagestyle{romano}
%\pagenumbering{arabic}
%\tableofcontents


%--------------------------------------------- 


%CONTENT


\newpage
\thispagestyle{plain}

\begin{center}
{\Large \textbf{Exercise Sheet 5}}
\end{center}

\noindent{\textbf{Exercise 5.1}}\\\\
a) free(P(a, y)) = vars(a) $\cup$ vars(y) = $\emptyset$ $\cup$ \{y\} = \{y\})\\\\
b)
free(P(x,y) $\wedge$ $\exists$ x  $\forall$ y (Q(x,y,z)))\\
= free(P(x,y)) $\cup$  free($\exists$ x  $\forall$ y (Q(x,y,z)))\\ 
= vars(x) $\cup$ vars(y) $\cup$  free(Q(x,y,z)) $\setminus$ \{x,z\}\\ 
= \{x, y\} $\cup$ \{y\} = \{x, y\}
\\\\
c) free($\exists$x (P(x, y) $\wedge$ Q(x)) $\vee$ P(y, x)) =\\
free(P(x, y) $\wedge$ Q(x)) $\vee$ P(y, x)) $\setminus$ \{x\}\\
free(P(x, y)) $\cup$ free(Q(x)) $\cup$ free(P(y, x)) $\setminus$ \{x\}\\
var(x) $\cup$ var(y) $\cup$ var(x) $\cup$ var(y) $\cup$ var(x) $\setminus$ \{x\} = \{y\}\\\\
d) free($\forall$ x ( $\exists$ y ( P(x, y) $\wedge$ Q(x)) $\vee$ P(x, y)))\\
 = free($\exists$ y ( P(x, y) $\wedge$ Q(x)) $\vee$ P(x, y)) $\setminus$ \{x\}\\
 = (free($\exists$ y ( P(x, y) $\wedge$ Q(x))) $\cup$ free(P(x, y))) $\setminus$ \{x\}\\
 = ((free(P(x, y) $\wedge$ Q(x)) $\setminus$ \{y\}) $\cup$ (vars(x) $\cup$ vars(y))) $\setminus$ \{x\}\\
 = ((free(P(x, y)) $\cup$ free(Q(x)) $\setminus$ \{y\}) $\cup$ \{x, y\}) $\setminus$ \{x\}\\
 = ((vars(x) $\cup$ vars(y) $\cup$ vars(x)) $\setminus$ \{y\}) $\cup$ \{x, y\}) $\setminus$ \{x\}\\
 = (\{x\} $\cup$ \{y\}) $\setminus$ \{x\} = \{y\}\\
\\\\
e) free ($\forall$x$\forall$y(P(x, b) $\wedge$ Q(x) $\vee$ P(f(y), x)))\\
free ((P(x, b) $\wedge$ Q(x) $\vee$ P(f(y), x))) $\setminus$ \{x, y\}\\
free ((P(x, b)) $\cup$ free(Q(x)) $\cup$ free(P(f(y), x)))) $\setminus$ \{x, y\}\\
var(x) $\cup$ var(b) $\cup$ var(x) $\cup$ var(f(y)) $\cup$ var(x) $\setminus$ \{x, y\}\\
var(x) $\cup$ var(b) $\cup$ var(x) $\cup$ var(y) $\cup$ var(x) $\setminus$ \{x, y\}\\
var(x) $\cup$ $\emptyset$ $\cup$ var(x) $\cup$ var(y) $\cup$ var(x) $\setminus$ \{x, y\} = $\emptyset$\\\\
f) free($\exists$ x ( $\exists$ z (R(x, z)) $\vee$ $\forall$ y (S(y,g(x, z)))))\\
 = free($\exists$ z (R(x, z)) $\vee$ $\forall$ y (S(y,g(x, z)))) $\setminus$ \{x\}\\
 = free(R(x, z) $\vee$ $\forall$ y (S(y,g(x, z)))) $\setminus$ \{x, z\}\\
 = (free(R(x, z)) $\cup$ free($\forall$ y (S(y,g(x, z))))) $\setminus$ \{x, z\}\\
 = ((vars(x) $\cup$ vars(z)) $\cup$ (free(S(y,g(x, z))) $\setminus$ \{y\}) ) $\setminus$ \{x, z\}\\
 = ( \{x,z\} $\cup$ (\{z,x,y\} $\setminus$ \{y\})) $\setminus$ \{x, z\}\\
 = \{x,z\} $\setminus$ \{x,z\} = $\emptyset$
\\\\
g) free($\exists$x($\exists$z(R(x, z))) $\vee$ $\forall$y(S(y, g(x, z))))\\
free($\exists$x($\exists$z(R(x, z))) $\cup$ free($\forall$y(S(y, g(x, z))))  \\
free($\exists$z(R(x, z))) $\setminus$ \{x\} $\cup$ free((S(y, g(x, z)))) $\setminus$ \{y\}\\
free((R(x, z))) $\setminus$ \{x, z\} $\cup$ free((S(y, g(x, z)))) $\setminus$ \{y\}\\
(var(x) $\cup$ var(z) $\setminus$ \{x, z\}) $\cup$ (var(y) $\cup$ var(g(x,z)) $\setminus$ \{y\})\\
$\emptyset$ $\cup$ (var(y) $\cup$ var(x)  $\cup$ var(z)) $\setminus$ \{y\}) = \{x,z\}\\

\vspace{1cm}
\noindent{\textbf{Exercise 5.2}}\\\\
We have to prove that all models of $\forall$x$\exists$y P(x,y) are models of $\exists$x P(f(z),x). For convenience I will refer to the first formula as $\varphi$ and to the second one as $\psi$\\
Since the domain is not given we can choose conveniently any domain.\\
Let's suppose then that the domain is D =\{d1\}.\\\\
There are only tow possible Interpretations I = (D, $^{.I}$)\\
1) $^{.I1}$ assigns the following meanings:\\
P=\{(d1,d1)\}\\
f(d1) = d1 (I have no chance, f(d1) must be mapped to the only element of the domain)\\
(there are no constants)\\
2) $^{.I2}$ assigns the following meanings:\\
P=$\emptyset$\\
f(z) = d1 (I have no chance, f(d1) must be mapped to the only element of the domain)\\
(there are no constants)\\\\
$\alpha$ =(x$\rightarrow$d1, y$\rightarrow$d1, z$\rightarrow$d1).  (I have no chance, the variables must be mapped to the only element of the domain).\\
I1 is a model for $\varphi$:\\
I1, $\alpha$ $\vDash$ $\forall$x$\exists$y P(x,y)\\
I1, $\alpha$ [x:=d1] $\vDash$ $\exists$y P(x,y)\\
I1, $\alpha$ [x:=d1][y:=d1] $\vDash$ P(x,y)\\
(d1, d1) $\in$ P$^{.I1}$\\\\
$^{.I1}$ is as well a model for $\psi$:\\
I1, $\alpha$ $\vDash$ $\exists$x P(f(z),x)\\
I1, $\alpha$ [x:=d1] $\vDash$ P(f(z),x)\\
(f(z), d1) $\in$ P$^{.I1}$\\
f(z)$^{.I1}$ = f$^{.I1}$(z$^{.I1}$) = f$^{.I1}$(d1) =d1\\
(d1, d1) $\in$ P$^{.I1}$\\\\
Using the same strategy, we know that I2 is not a model for $\varphi$ because (d1, d1) $\notin$ P$^{.I2}$. The same holds for $\psi$.
Therefore we can state that all the models of $\varphi$ are also the models of $\psi$.


\vspace{1cm}
\noindent{\textbf{Exercise 5.3}}\\\\
a)
By definition of the equivalence we must show that both $\neg \forall x \phi \models \exists x \neg \phi$ and $\exists x \neg \phi \models \neg \forall x \phi$.\\
Let $\varphi = \neg \forall x \phi$ and $\phi =  \exists x \neg \phi$\\
1. $\neg \forall x \phi \models \exists x \neg \phi$\\
Suppose we have a model for $\varphi$. For this model $\forall x \phi$ must be false. This means there is a x for which $\phi$ doesn't hold. For that x:  $\neg \phi$ must be true. Hence it's a model of $\psi$.\\
2. $\exists x \neg \phi \models \neg \forall x \phi$\\
Suppose there's a model for $\psi$. This means there is a x for which $\neg \phi$ is true. This means $\phi$ is false for that very x. Hence $\forall x \phi$ can't hold for all x, which makes $\varphi$ true and it's also a model.\\ 

b) The counter example consists in an Interpretation which satisfies the first formula but not the second, violating the definition of equivalence.\\
Let's assume that:\\
$\phi$ = P(x,y), D=\{d1,d2\}\\
P =\{(d1,d1), (d2,d2)\}\\\\
It is not necessary to consider a variables' assignment because both formulas are closed.\\
In this case the interpretation satisfies $\forall$x$\exists$y $\phi$:\\
I[x:=d1] $\vDash$ $\exists$y P(x,y) $\wedge$ I[x:=d2] $\vDash$ $\exists$y P(x,y)\\
(I[x:=d1][y:=d1] $\vDash$ P(x,y) $\vee$ I[x:=d1][y:=d2] $\vDash$ P(x,y)) $\wedge$\\
(I[x:=d2][y:=d1] $\vDash$ P(x,y) $\vee$ I[x:=d2][y:=d2] $\vDash$ P(x,y))\\
((d1, d1) $\in$ P$^{.I1}$ $\vee$ (d1, d2) $\in$ P$^{.I1}$) $\wedge$\\
((d2, d1) $\in$ P$^{.I1}$ $\vee$ (d2, d2) $\in$ P$^{.I1}$)\\
which is true because (d1,d1), (d2,d2) $\in$  P$^{.I1}$.\\\\
However, the interpretation doesn't satisfies $\exists$y$\forall$x $\phi$:\\
I[y:=d1] $\vDash$ $\forall$x P(x,y) $\vee$ I[y:=d2] $\vDash$ $\forall$x P(x,y)\\
(I[y:=d1][x:=d1] $\vDash$ P(x,y) $\wedge$ I[y:=d1][x:=d2] $\vDash$ P(x,y)) $\vee$\\
(I[y:=d2][x:=d1] $\vDash$ P(x,y) $\wedge$ I[y:=d2][x:=d2] $\vDash$ P(x,y))\\
((d1, d1) $\in$ P$^{.I1}$ $\wedge$ (d2, d1) $\in$ P$^{.I1}$) $\vee$\\
((d1, d2) $\in$ P$^{.I1}$ $\wedge$ (d2, d2) $\in$ P$^{.I1}$)\\
which is not true because (d2,d1) and (d1,d2) $\notin$ P$^{.I1}$ making the $\vee$ false.\\\\
Since the interpretation satisfies the left formula but not the right one, it is proven that the formulas are not equivalent.
\end{document}

